『Homotopy Type Theory 入門』

1. どんなもの？

type-chekingを決定可能にしたい？

2. 先行研究と比べてどこがすごい？

3. 技術や手法のキモはどこ？

4. どうやって有効だと検証した？

5. 議論はある？

6. 次に読むべき論文は？

7. 参考文献

Alvaro Pelayo and Michael Warren. 『Homotopy type theory and Voevodsky's univalent foundations』. Bulletin of the American Mathematical Society, 51(4):597–648, 2014. arXiv:1210.5658v1, doi:10.1090/s0273-0979-2014-01456-9

1. イントロダクション

同型な型を等しいとみなしてよいことを保証する公理

帰納的型の拡張で、単位円周や球面などの空間を表す型や、自由群や商型などの要素間の同一視が必要な型を構成できる

1.1 型と空間

Univalent Foundations program

HoTT の基本的なアイディアは、型を空間、要素を点と解釈すること

等式型 a =A a′ を点 a から点 a′ への道の空間

uniqueness of identity proofs (UIP)

数学的対象$ a が型$ a を持つことを$ a : A

$ a は型$ A の要素であるとも言う

$ a は変数$ x に依存するかもしれないときは$ a[x] と書く

代入(substitution)という操作でもある

二つの数学的対象が等しい場合は$ a \equiv b

型$ A, B 、$ A から$ B への関数型(function type)を$ A \to B

$ x : A

変数$ x : A 、要素$ b[x] : B があったときに、λ-抽象は

$ λ(x : A).b[x] : A \to B

要素$ f : A \to B と$ a : A があったときに、関数適用(application)$ f(a) : A \to B が定義される

α同値

β同値

η同値